<theory> A set of assertions about properties of a system and how they are effected by program execution. The axiomatic semantics of a program could include pre- and post-conditions for operations. In particular if you view the program as a state transformer (or collection of state transformers), the axiomatic semantics is a set of invariants on the state which the state transformer satisfies. E.g. for a function with the type: sort_list :: [T] -> [T] we might give the precondition that the argument of the function is a list, and a postcondition that the return value is a list that is sorted. One interesting use of axiomatic semantics is to have a language that has a finitely computable sublanguage that is used for specifying pre and post conditions, and then have the compiler prove that the program will satisfy those conditions. See also operational semantics, denotational semantics. (1995-11-09)

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax.

Semantics (from (semantikos), "related to meaning, significant", from semaino, "to signify, to indicate", which is from sema, "sign, mark, token". The plural is used in analogy with words similar to physics, which was in the neuter plural in Ancient Greek and meant "things relating to nature".

<theory> The meaning of a string in some language, as opposed to syntax which describes how symbols may be combined independent of their meaning. The semantics of a programming language is a function from programs to answers. A program is a closed term and, in practical languages, an answer is a member of the syntactic category of values. The two main kinds are {denotational semantics} and operational semantics. (1995-06-21)